\documentclass[a4paper,10pt]{article}

\usepackage{amsfonts, amsmath, amsthm, amssymb}
\usepackage[english]{babel}
%\usepackage{bookman}
%\usepackage{pxfonts}

%\usepackage[T1]{fontenc}
\usepackage{subfig}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage{a4wide}
\pagestyle{headings}	
\pagestyle{plain}
\usepackage{hyperref}

\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}

\newcommand{\mint}[1]{\mathrm{#1}}
\newcommand{\then}{\Rightarrow}


%\frenchspacing

\title{Automatic reasoning, assignment 2 \\ Solitaire}
\author{Niklas Weber \\ 0841420, \\ Matúš Tejiščák \\ 4176200}
\date{\today}

\begin{document}

\maketitle

\section{Representation of the game model}

\subsection{Variables}

We represent a single state of board of size $N \times N$ (and actions taken) by the following
collections of variables:
\begin{itemize}
	\item $S_{ij}$ is $\true$ iff there is a stone at the position $(i,j)$;
	\item $V = [v_i]$ represents the vertical coordinate of the \emph{selected stone}
		(ranging from $1$ to $N$);
	\item $H = [h_i]$ represents the horizontal coordinate of the \emph{selected stone}
		(ranging from $1$ to $N$);
	\item $d$ is the direction of skipping ($\true$ = horizontal, $\false$ = vertical);
	\item $s$ is the sign of skipping ($\true$ = towards higher coordinate values,
		$\false$ = towards lower coordinate values);
	\item $T = [t_i]$ is the number of steps taken from the beginning of the game.
\end{itemize}
The phrase \emph{selected stone} denotes (intuitively) the stone that will "skip" over its neighbor
to get from the current state to the next one (see Figure \ref{fig:selected}).

\begin{figure}[htp]
	\begin{center}
		\includegraphics[width=0.5\textwidth]{task2-selected}
	\end{center}
	\caption{Selected stone (red) "skipping" in different directions.}
	\label{fig:selected}
\end{figure}

Since we want to create a purely Boolean encoding of the problem, we will have to encode the integral
variables in binary. For this purpose, for each variable $X$, we introduce a sequence of
boolean variables $x_i$, along with the square-bracket notation:
\[ X = \sum_i 2^i x_i = [x_i] \mint{,} \]
where we implicitly identify $\true$ with $1$ and $\false$ with $0$. In practice, we limit the number
of the bits in question to $K = \lceil \log_2 (\mathsf{maxval}(X)+1) \rceil$.

In total, having a $N \times N$-sized board, we get
$N^2 + 3K + 2 = O(N^2)$ boolean variables.

The collection of  boolean variables $S_{ij}$ and $t_i$ describes the state of the playing board;
the variables
$V, H, d, s$ are nondeterministically chosen by the solver: they represent
the step taken by the player. Then $T'$ in the next step deterministically depends only on $T$
in the previous step; $S'_{ij}$ in the next step depends deterministically on
$S_{ij}, V, H, d$, and $s$ in the following way.

\subsection{Rules/clauses}

\subsubsection{Initial state}

The initial state is described by the following set of rules:
\begin{align}
	& [t_i] = 0
		& \text{(We start at the zero time.)} \\
	\bigwedge_{1 \leq i,j \leq N} & S_{ij} \Longleftrightarrow i \neq 3 \vee j \neq 3
		& \text{(Only the middle square is unoccupied.)}
\end{align}

\subsubsection{State transition}

First, let us list the short rules. 

\begin{align}
	\bigvee_{k=1}^{24-R} [t'_i] &= k-1 \wedge [t_i] = k
		& \text{(Time advances.)} \\
	\bigvee_{1 \leq i,j \leq N} [v_k] &= i \wedge [h_k] = j 
		& \text{($V$ and $H$ point into the board)} \\
	\bigwedge_{1 \leq i,j \leq N} [v_k] &= i \wedge [h_k] = j
		\; \Longrightarrow \; S_{ij} \wedge \neg S'_{ij} 
		& \text{(Stone removed from $(V,H)$.)} \\
\end{align}

The variables describing the new state always carry
a prime, that is, $S_{ij}$ belongs to the old state, $S'_{ij}$ belongs to the new state.
Let us continue with the jumping rule.

\begin{align}
	\bigvee &
	\left\lbrace \begin{array}{rl} 
		d \wedge      s \wedge
			& \displaystyle \bigvee_{\substack{1 \leq i \leq N \\ 1 \leq j \leq N-2}} 
			B(i,j,0,+1) \vspace{2mm} \\
		d \wedge \neg s \wedge
			& \displaystyle \bigvee_{\substack{1 \leq i \leq N \\ 3 \leq j \leq N}}
			B(i,j,0,-1) \vspace{2mm} \\
		\neg d \wedge      s \wedge
			& \displaystyle \bigvee_{\substack{1 \leq i \leq N-2 \\ 1 \leq j \leq N}}
			B(i,j,+1,0) \vspace{2mm} \\
		\neg d \wedge \neg s \wedge
			& \displaystyle \bigvee_{\substack{3 \leq i \leq N \\ 1 \leq j \leq N}}
			B(i,j,-1,0)
	\end{array} \right. & \text{(Four directions, four branches.)}
\end{align}

Here, for each direction (and each possible position) of we need to determine the next state of
the board. There are four directions the player could move in;
for every one of the four directions, there are $(N-2)^2$ stones that could be picked as
\emph{selected} (and we need to expand on that because we are working in a first-order theory).
\emph{At least} one of these possibilities must be true, hence the disjunctions. Also,
\emph{at most} one of these possibilities must be true but this is taken care of by the fact
that the possibilities themselves are mutually exclusive by their nature ($d$, $s$, $v_i$, $h_i$
are exactly determined in each).

Now we need to describe what rules must be observed in each of these four branches.
First, the selected stone must match. Then we describe how stones are affected by the skip.
Finally, we describe how the unaffected stones are carried to the new state unchanged.
\begin{align}
	B(i,j,p,q) &= [v_k] = i \wedge [h_k] = j \wedge A(i,j,p,q) \wedge U(i,j,p,q) \\
	A(i,j,p,q) &= S_{i+p,j+q} \wedge \neg S_{i+2p,j+2q}
		\wedge \neg S'_{i+p,j+q} \wedge S'_{i+2p,j+2q} \\
	U(i,j,p,q) &= \bigwedge_{1 \leq k,l \leq N}
		\underbrace{(k,l) \notin \{(i,j),(i+p,j+q),(i+2p,j+2q)\}}_{\text{unaffected}}
		\Longrightarrow
		S_{kl} \Leftrightarrow S'_{kl}
\end{align}

The nested quantifier used to describe the unaffected stones in $U(i,j,p,q)$ causes the
total number of clauses to blow up to $O(N^4)$.

\subsubsection{Final state}

If we denote the required number of stones to remain on the board $R$, then the final state
must satisfy this condition:
\begin{equation}
	[t_i] = 24 - R
\end{equation}
This exploits the fact that in each step we get exactly one stone off the board.

Furthermore, we must be unable to make another step. This is similar to the (reduced) transition
specification -- we must prove that none of the four possible movements from any selected square
is possible (this proposition is called \textsf{deadEnd} in the Haskell program).

\begin{align}
	\neg \bigvee &
	\left\lbrace \begin{array}{rl} 
			\displaystyle \bigvee_{\substack{1 \leq i \leq N \\ 1 \leq j \leq N-2}} 
			&P(i,j,0,+1) \vspace{2mm} \\
			\displaystyle \bigvee_{\substack{1 \leq i \leq N \\ 3 \leq j \leq N}}
			&P(i,j,0,-1) \vspace{2mm} \\
			\displaystyle \bigvee_{\substack{1 \leq i \leq N-2 \\ 1 \leq j \leq N}}
			&P(i,j,+1,0) \vspace{2mm} \\
			\displaystyle \bigvee_{\substack{3 \leq i \leq N \\ 1 \leq j \leq N}}
			&P(i,j,-1,0)
	\end{array} \right. \text{ \textbf{where} } \bigg [
	P(i,j,p,q) = S_{ij} \wedge S_{i+p,j+q} \wedge S_{i+2p,j+2q} \bigg ]
\end{align}

\subsection{Total number of clauses and variables}

\begin{itemize}
	\item $N^2 + 3K + 2 = O(N^2)$ Boolean variables
	\item $O(N^2) + O(N^4) + O(N^2) = O(N^4)$ clauses (initial state + transition + final state)
\end{itemize}
In total, we have $O(N^4)$ clauses and $O(N^2)$ Boolean variables.

\section{Implementation of the model}

\subsection{Binary encoding}

In our program, we only have binary encoding constraints of the shape
\begin{equation}
	[x_i] = X \mint{,}
\end{equation}
where $x_i$ is a collection of Boolean variables and $X$ is an integer. This can be
represented as
\begin{equation}
	\bigwedge_{0 \leq i \leq K-1} x_i \Longleftrightarrow \mathsf{bit}(X,i) = 1 \mint{.}
\end{equation}
Take, for example, $X = 11_{10} = 01011_{2}$. This translates to the following formula:
\begin{equation}
	\neg x_4 \wedge x_3 \wedge \neg x_2 \wedge x_1 \wedge x_0
\end{equation}
Furthermore, addition occurs in only one place in our program and even there it is the addition
of $1$. Instead of devising elaborate addition algorithms, we simply hardcode a table:
\begin{equation}
	\bigwedge_{1 \leq i \leq N^2} [t_i] = i-1 \Longrightarrow [t'_i] = i \mint{,}
\end{equation}
which translates to a collection of $N^2$ implications, exactly one applicable in each step.

\subsection{Variable ordering}

Since we use \textsf{bddsolve} for this problem, we also need to specify the order of variables.
We picked this order: $t_i$, $d$, $s$, $v_i$, $h_i$, $S_{ij}$, going from most the constrained
variables ($t_i$ is completely determined by a single meta-variable in the previous step),
through the variables that are valuated nondeterministically ($d$, $s$, $v_i$, and $h_i$) to
$S_{ij}$, that depends on the choice of all other variables.

\subsection{Implementation languages}

The bulk of the work was done in \textsf{Haskell}\footnote{
	\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/Task2-bdd.hs}
} using a specialized EDSL, which enabled us
to write the formulas in the same form as they appear in this paper. Expansion into first-order
formulas is done by the machinery underneath.

Since \textsf{bddsolve} uses a bit quirky way of naming variables (which is completely
understandable for small formulas but less suitable for larger developments), we also used
a small \textsf{Perl} program\footnote{
	\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/Task2-mogrify.pl}
} to change systematical variable names to their
\textsf{bddsolve}-compatible counterparts. This program also computes the ordering of variables
given to \textsf{bddsolve}.

\section{Solving the questions}

We used \textsf{bddsolve} along with the \textsc{Reach} logic to solve the formulas described
in this paper. \textsf{Bddsolve} proceeded safely over iterations and in a short time it
gave results.

\begin{description}
	\item[Is it possible to end with three stones?] ~ \\
		Yes, it is. See Figure \ref{fig:sample-game-3} on page \pageref{fig:sample-game-3}
		for one of the possible game paths. Ending with three separated stones in the bottom
		line, there is no way to continue from that position.
		
	\item[Is it possible to end with two stones?] ~ \\
		Yes, a two-stone ending is reachable as well, as shown in the Figure \ref{fig:sample-game-2}
		on page \pageref{fig:sample-game-2}.
	
	\item[Is it possible to end with only one stone?] ~ \\
		No. For one stone, \textsf{bddsolve} reports unsatisfiability of the problem, hence
		square peg solitaire with the usual rules (exactly one stone left) is unsolvable from our
		starting position. However,
		if we had started from a little different initial position (where the empty position would
		be off-center by one square, in one of the four directions), the game would	have been
		solvable.
\end{description}


\newpage
\subsection{Figures}
\begin{figure}[htp]
	\include{task2-appendix-3}
	\caption{An example game ending in three stones on the board.}
	\label{fig:sample-game-3}
\end{figure}

\begin{figure}[htp]
	\include{task2-appendix-2}
	\caption{An example game ending in two stones on the board.}
	\label{fig:sample-game-2}
\end{figure}

\end{document}




























